open structures
open cic
open eap
open ease
open nd
open s

// ------------------------------------------------------------
//  EA - Element Architecture
// ------------------------------------------------------------

one sig EA_ClientStub extends EA {}
fact EA_ClientStub {
	all ei: FullFledgedEA | ei.ea = EA_ClientStub => {
		AvailablePorts[ei, EAPLP_CallIn + EAPR_MW]
		SubElements[ei, EASE_Logger + EASE_Stub]

		let ei_logger =  ei.subElements[EASE_Logger] |
		let ei_stub = ei.subElements[EASE_Stub] {
			AllowedEAsForSublement[ei_logger, EA_FileLogger]
			DelegateDeployment[ei, ei_logger]

			AllowedEAsForSublement[ei_stub, EA_RMIStub]
			DelegateDeployment[ei, ei_stub]

			PortBinding[ei, EAPLP_CallIn, ei_logger, EAPLP_CallIn]
			PortBinding[ei_logger, EAPLR_CallOut, ei_stub, EAPLP_CallIn]
			PortBinding[ei_stub, EAPR_MW, ei, EAPR_MW]
		}
	}
}

one sig EA_FileLogger extends EA {}
fact EA_FileLogger {
	all ei: FullFledgedEA | ei.ea = EA_FileLogger => {
		AllowedDeployment[ei, ND_A]
		AvailablePorts[ei, EAPLP_CallIn + EAPLR_CallOut]
		no ei.subElements

		-- port signature delegation
		ei.portSignatures[EAPLP_CallIn] = ei.portSignatures[EAPLR_CallOut]
		-- definition of features and attributes
		//ProvidedFeatures[ei, FT_Logging]
		//AvailableAttributes[ei, AT_FileName]
		-- assignment of features
		//AssignFeatureValue[ei, FT_Logging, FV_Logging_ToFile]
		//AssignAttributeValue[ei, FT_Logging, filename, AT_FileName]
	}
}

one sig EA_ConsoleLogger extends EA {}
fact EA_ConsoleLogger {
	all ei: FullFledgedEA | ei.ea = EA_ConsoleLogger => {
		AvailablePorts[ei, EAPLP_CallIn + EAPLR_CallOut]
		no ei.subElements

		ei.portSignatures[EAPLP_CallIn] = ei.portSignatures[EAPLR_CallOut]
	}
}

one sig EA_RMIStub extends EA {}
fact EA_RMIStub {
	all ei: FullFledgedEA | ei.ea = EA_RMIStub => {
		AvailablePorts[ei, EAPLP_CallIn + EAPR_MW]
		no ei.subElements

		ei.portSignatures[EAPR_MW] = S_RMI
		all s: S_RMI | ei.portSignatures[EAPR_MW] = s => {
			s.javaSig = ei.portSignatures[EAPLP_CallIn]
			s.sockType = S_SSL
		}
	}
}

one sig EA_ServerSkeleton extends EA {}
fact EA_ServerSkeleton {
	all ei: FullFledgedEA | ei.ea = EA_ServerSkeleton => {
		AvailablePorts[ei, EAPLR_CallOut + EAPR_MW]
		SubElements[ei, EASE_Skeleton + EASE_Serializer]

		let ei_skeleton =  ei.subElements[EASE_Skeleton] |
		let ei_serializer = ei.subElements[EASE_Serializer] {
			AllowedEAsForSublement[ei_skeleton, EA_SecureSkeleton]
			DelegateDeployment[ei, ei_skeleton]
			AvailablePorts[ei_skeleton, EAPR_MW + EAPLR_CallOut]

			AllowedEAsForSublement[ei_serializer, EA_CallSerializer]
			DelegateDeployment[ei, ei_serializer]
			AvailablePorts[ei_serializer, EAPLP_CallIn + EAPLR_CallOut]

			PortBinding[ei, EAPR_MW, ei_skeleton, EAPR_MW]
			PortBinding[ei_skeleton, EAPLR_CallOut, ei_serializer, EAPLP_CallIn]
			PortBinding[ei_serializer, EAPLR_CallOut, ei, EAPLR_CallOut]
		}
	}
}

one sig EA_SecureSkeleton extends EA {}
fact EA_SecureSkeleton {
	all ei: FullFledgedEA | ei.ea = EA_SecureSkeleton => {
		AvailablePorts[ei, EAPLR_CallOut + EAPR_MW]
		SubElements[ei, EASE_Skeleton + EASE_Socket]

		let ei_skeleton =  ei.subElements[EASE_Skeleton] |
		let ei_socket = ei.subElements[EASE_Socket] {
			AllowedEAsForSublement[ei_skeleton, EA_RMISkeleton]
			DelegateDeployment[ei, ei_skeleton]
			AvailablePorts[ei_skeleton, EAPR_MW + EAPLR_CallOut + EAPLR_FactoryOut]

			AllowedEAsForSublement[ei_socket, EA_SocketFactoryProvider]
			DelegateDeployment[ei, ei_socket]
			AvailablePorts[ei_socket, EAPLP_FactoryIn]

			PortBinding[ei, EAPR_MW, ei_skeleton, EAPR_MW]
			PortBinding[ei_skeleton, EAPLR_CallOut, ei, EAPLR_CallOut]
			PortBinding[ei_skeleton, EAPLR_FactoryOut, ei_socket, EAPLP_FactoryIn]
		}
	}
}

one sig EA_RMISkeleton extends EA {}
fact EA_RMISkeleton {
	all ei: FullFledgedEA | ei.ea = EA_RMISkeleton => {
		AvailablePorts[ei, EAPLR_CallOut + EAPLR_FactoryOut + EAPR_MW]
		no ei.subElements

		//ei.portSignatures[EAPLR_CallOut] = $I
		ei.portSignatures[EAPR_MW] = S_RMI
		all s: S_RMI | ei.portSignatures[EAPR_MW] = s => { s.javaSig = ei.portSignatures[EAPLR_CallOut] }
		ei.portSignatures[EAPLR_FactoryOut] = S_SocketFactoryProv
		all s: S_SocketFactoryProv, s': S_RMI | ei.portSignatures[EAPLR_FactoryOut] = s and ei.portSignatures[EAPR_MW] = s' => { s.sockType = s'.sockType }
		//ei.portSignatures[EAPLR_Factory].sockType = 
	}
}

one sig EA_SocketFactoryProvider extends EA {}
fact EA_SocketFactoryProvider {
	all ei: FullFledgedEA | ei.ea = EA_SocketFactoryProvider => {
		AvailablePorts[ei, EAPLP_FactoryIn]
		no ei.subElements

		ei.portSignatures[EAPLP_FactoryIn] in S_SocketFactoryProv
		ei.portSignatures[EAPLP_FactoryIn].(S_SocketFactoryProv <: sockType) in S_SSL // XXX TODO: + S_PlainText
	}
}

one sig EA_CallSerializer extends EA {}
fact EA_CallSerializer {
	all ei: FullFledgedEA | ei.ea = EA_CallSerializer => {
		AvailablePorts[ei, EAPLR_CallOut + EAPLP_CallIn]
		no ei.subElements

		ei.portSignatures[EAPLP_CallIn] = ei.portSignatures[EAPLR_CallOut]
	}
}

pred SubElements[ffea: FullFledgedEA, elements: set EASE] {
	ffea.subElements.univ = elements
}

pred AllowedDeployment[ffea: FullFledgedEA, nodes: set ND] {
	ffea.node in nodes
}

pred AllowedEAsForSublement[ffea: FullFledgedEA, allowedEAs: set EA] {
	ffea.ea in allowedEAs
}

pred DelegateDeployment[from: FullFledgedEA, to: FullFledgedEA] {
	to.node = from.node
}

pred AvailablePorts[ffea: FullFledgedEA, availablePorts: set EAP] {
	ffea.portSignatures.univ = availablePorts
}

pred PortBinding[ffea1: FullFledgedEA, p1: EAP, ffea2: FullFledgedEA, p2: EAP] {
	ffea1.portSignatures[p1] = ffea2.portSignatures[p2]
}

